#include "qpf.h"
#include "Sort.h"
#include <iostream>
#include <fstream>
#include <cassert>

using std::cout;
using std::endl;
extern std::ostream & operator<<( std::ostream & out , const MinisatProof::Lit & l );

//=============================================================================
//      Profiling 
//=============================================================================
//
//  print clause 
//
template< class T > 
static void print( const MinisatProof::vec<T> & t )
{
   for( int i = 0 ; i < t.size() ; ++i ) 
      cout<<t[i]<<" ";
   cout<<endl;
}
//
// check the variable is inside the clause , return the sign of lit , -1 means no 
//
static int check_exist( const cls_t & c , int x)
{
   for( int i = 0 ; i < c.size() ; ++ i )
      if( var(c[i])== x)return sign(c[i]);
   return -1;
}
//
// check equivalence
//
static bool check_eq( const cls_t & a , const cls_t & b )
{
   for( int i = 0 ; i < a.size() ; ++i )
   {
      int cnt = 0; 
      for( int j = 0 ; j < b.size() ; ++ j ) 
         if( a[i] == b[j] ) 
            cnt +=1;
      
      if( cnt != 1 ) return false ;
   }
   return true;
}
//
//  resolve without lut 
//
static void check_resolve( const cls_t & a , const cls_t & b , cls_t & c , plit_t x )
{
   assert( c.size() == 0 );
   assert( check_exist( a , var(x) ) ==  sign(x) );
   assert( check_exist( b , var(x) ) == (sign(x)^1) );
   for( int i = 0 ; i < a.size() ; ++ i ) if ( a[i] != x ) c.push(a[i]);
   for( int i = 0 ; i < b.size() ; ++ i ) if ( b[i] != ~x ) c.push(b[i]);
   sortUnique( c );
}
//
//  resolve clause from a and b to clause c by the lit x in a and ~x in b , lut is buf
//
static void resolve( const cls_t & a , const cls_t & b , cls_t & c , plit_t x , unsigned * lut )
{
   assert( c.size() == 0 );
   assert( check_exist( a , var(x) ) ==  sign(x) );
   assert( check_exist( b , var(x) ) == (sign(x)^1) );

   c.growTo( a.size() + b.size() );
   int j = 0;
   
   for( int i = 0 ; i < a.size() ; ++i )
   {
      lut[ var(a[i]) ] = 1<<sign(a[i]);
      if( a[i] != x )
         c[j++] = a[i];
   }
   for( int i = 0 ; i < b.size() ; ++i )
   {
      if( lut[ var(b[i]) ] == 0 )
         c[j++] = b[i];
      else
      {
         assert( (lut[ var(b[i]) ] == (unsigned)(1<<sign(b[i])) ) || (b[i] == ~x ) );
      }
   }
   c.shrink( c.size() - j ); // resize to j 
   for( int i = 0 ; i < a.size() ; ++i )
      lut[ var(a[i]) ]=0;
   lut[ var(x) ] = 0;
}

//=============================================================================
//      Clause member function
//=============================================================================

// soft recycle 
vector<Clause * > Clause::DEL_BOX;
void Clause::remove()
{
   //assert( this->del == 0 );
   if( del ) return ;
   
   if( isLeaf() == false )
   {
      in[0]->remove_output( this );
      in[1]->remove_output( this );
   }
   this->del = 1;
   DEL_BOX.push_back( this );
}
void Clause::remove_remove()
{
   for( unsigned i = 0 ; i < DEL_BOX.size() ; ++i )
   {
      assert( DEL_BOX[i]->del ==1 );
      delete DEL_BOX[i];
   }
   DEL_BOX.clear();
}
Clause::Clause( Clause * a , Clause * b , plit_t _x , unsigned * lut )
   :x(_x),mrk(0),del(0)
{
   in[0] = a , in[1] = b;
   resolve( *a , *b , *this , _x , lut );
   a->out.push_back( this );
   b->out.push_back( this );
}
void Clause::remove_output( Clause * t )
{
   assert( out.size() );
   for( unsigned i = 0 ; i < out.size() ; ++ i )
      if( out[i] == t )
         std::swap( out[i] , out.back() );
   assert( out.back() == t );
   out.pop_back();

   if( out.size() == 0 ) remove( );
}
void Clause::change_input( Clause * from , Clause * to )
{
   to->out.push_back( this );

   if( in[0] == from ) 
      in[0] = to;
   else 
   {
      assert( in[1] == from );
      in[1] = to;
   }

   from->remove_output( this ); 
}
void Clause::replace( Clause * to )
{
   assert( to != this );
   while( out.size() )
      out[0]->change_input( this , to );
   remove();
}
bool Clause::inorder( const unsigned * lvl )const
{
   if( isLeaf() )return true;

   unsigned l = lvl[ var(x) ];
   for( int i = 0 ; i < size() ; ++ i )
      if( l > lvl[ var( (*this)[i] ) ] ) return false;
   return true;
}
bool Clause::check_resolve( )const
{
   if( isLeaf() ) return true;
   cls_t t;
   ::check_resolve( *(in[0]) , *(in[1]) , t , x );
   return check_eq( *this , t );
}
bool Clause::check_connect( )const
{
   for( unsigned i = 0 ; i < out.size(); ++ i )
      if( out[i]->in[0] != this && out[i]->in[1] != this )
         return false;
   return true;
}
void Clause::plot( std::ostream & o )const
{
   o << "_"<< this << "[label=\"";
   if( isLeaf() == false ) o << "[" << var(x) <<"]";
   for( int i = 0 ; i < size() ; ++ i )
      o << (*this)[i] << " ";
   o<<"\"];"<<endl;
   if( isLeaf() ) return;

   o << "_"<<in[0]<<" -- _"<<this<<";"<<endl;
   o << "_"<<in[1]<<" -- _"<<this<<";"<<endl;
}
bool Clause::slim( unsigned * lut )
{
   for( int j = 0 ; j < 2 ; ++ j )
      for( int i = 0 ; i < in[j]->size() ; ++ i)
         lut[ var( (*(in[j]))[i] ) ] = 1;

   int j = 0;
   for( int i = 0 ; i < size() ; ++ i )
      if( lut[var( (*this)[i] ) ] != 0 )
         (*this)[j++] = (*this)[i];

   for( int j = 0 ; j < 2 ; ++j )
      for( int i = 0 ; i < in[j]->size() ; ++ i )
         lut[ var( (*(in[j]))[i] ) ] = 0;

   if( j == size() ) return false;
   shrink( size() - j );
   return true;
}
void Clause::interpolant( StrashAIG & ckt , int * base )
{
   if( isLeaf() ) 
   {
      if( isA() ) itp = toAigLit( 0 , 0 );
      else        itp = toAigLit( 0 , 1 );
   }else
   {
      int b = base[ var(x) ];
      if( b < 0 )
      {
         if( b == -1 ) //Local A
            itp = inv( ckt.createAND( inv( in[0]->itp ) , inv( in[1]->itp ) ) );
         else 
            itp = ckt.createAND( in[0]->itp , in[1]->itp );
      }else
      {
         AigLit sel = toAigLit( b , sign(x)^1 );
         AigLit pos = ckt.createAND( sel , in[0]->itp );
         AigLit neg = ckt.createAND( inv(sel) , in[1]->itp );
         itp = inv( ckt.createAND( inv(pos) , inv(neg) ) );
      }
   }
}
//=============================================================================
//      Function Objects
//=============================================================================

struct check_resolve
{
   void operator()( const Clause * c )const{
      if( c->check_resolve() == false ){
         cout << "Error" <<endl;exit(1);
      }
   }
};
struct check_connect
{
   void operator()( const Clause * c )const{ 
      if( c->check_connect() == false){
         cout << "Error" <<endl;exit(1);
      }
   }
};
struct check_inorder
{
   void operator()( const Clause * c )const{ 
      if( c->inorder( lvl) == false){
         cout << "Error" <<endl;exit(1);
      }
   }
   check_inorder( const unsigned * l):lvl(l){}
   const unsigned * lvl;
};
struct report_cls
{ 
   void operator()( const Clause * c )const{ n+=1 , e+=c->out.size() , r+=c->isLeaf();};  
   report_cls():n(0),e(0),r(0){}
   void print()const{ cout << "Node="<<n<<"\tEdge="<<e<<"\tRoot="<<r<<endl; }
   mutable unsigned n ,e ,r ;
};
struct plot
{
   void operator()( const Clause * c )const{c->plot( out); }
   plot( std::ostream & o ):out(o){};
   std::ostream & out;
};
struct get_branch
{
   void operator()( Clause * c )const{ if( c->isLeaf() == false) v.push_back( c ); }
   vector< Clause * > & v;
   get_branch( vector<Clause *> & _v ):v(_v){}
};
struct get_cls
{
   void operator()( Clause *c )const{ v.push_back( c );}
   vector< Clause * > & v ;
   get_cls( vector<Clause * > & _v ):v(_v){}
};
struct interpolant
{
   void operator()( Clause * c ) const 
   {
      assert( c->isLeaf() || ( c->in[0]->mrk != 0 && c->in[1]->mrk != 0 ) );
      c->interpolant(ckt,base);
   }
   interpolant( StrashAIG & c , int * b ):ckt(c),base(b){}
   StrashAIG & ckt;
   int       * base;
};
//=============================================================================
//      ProofTraverser 
//=============================================================================

void QProof::root( const cls_t & c , uint8_t x )
{
   assert( x == 0 || x == 1 ); // 0 is B 1 is A
   Clause * nc = new Clause( x==1 );
   c.copyTo( *nc );
   _cls.push_back( nc );
}
void QProof::chain  (const MinisatProof::vec<int> & cs, const cls_t & xs)
{
   Clause * x = _cls[ cs[0] ];
   for( int i = 0 ; i < xs.size() ; ++ i )
      x = this->resolve( x , _cls[ cs[i+1] ], xs[i] );
   _cls.push_back( x ); 
}
Clause * QProof::resolve( Clause * a , Clause * b , plit_t x )
{
   return new Clause( a , b , x , _lut );
}
void QProof::done(){
   _root = _cls.back();
   for( unsigned i = 0 ; i < _cls.size() - 1  ; ++i )
   {
      if( _cls[i]->out.size() == 0 )
         _cls[i]->remove();
   }
   Clause::remove_remove();
}

//=============================================================================
//      traversing template
//=============================================================================

template<class T>
static void clause_preorder( const T & t , Clause * c , uint8_t m = 1)
{
   if( (c->mrk&m) ) return;
   c->mrk |= m;
   t(c);
   if( !c->isLeaf() )clause_preorder( t , c->in[0] , m );
   if( !c->isLeaf() )clause_preorder( t , c->in[1] , m );
}
template<class T>
static void clause_postorder( const T & t , Clause * c , uint8_t m = 1)
{
   if( (c->mrk&m) ) return;
   c->mrk |= m;
   if( !c->isLeaf() )clause_postorder( t , c->in[0] , m );
   if( !c->isLeaf() )clause_postorder( t , c->in[1] , m );
   t(c);
}
static void clear_mrk( Clause * c )
{
   if( c->mrk == 0 ) return ;
   c->mrk = 0;
   if( c->isLeaf() )return;
   clear_mrk( c->in[0] );
   clear_mrk( c->in[1] ); 
}

//=============================================================================
//      QProof member function
//=============================================================================

void QProof::init( unsigned n)
{
   _lut = new unsigned [n]; 
   _lvl = new unsigned [n];
   memset( _lvl , 0 , sizeof(unsigned)*n);
   memset( _lut , 0 , sizeof(unsigned)*n); 
}
QProof::~QProof()
{
   clear_mrk( _root );
   vector<Clause * > c;
   clause_preorder( get_cls(c) , _root );
   for( unsigned i = 0 ; i < c.size() ;++i )
      delete c[i];
   delete [] _lut;
   delete [] _lvl;
}
void QProof::report()const
{
   clear_mrk( _root );
   report_cls rep;
   clause_preorder( rep , _root );
   rep.print();
}
void QProof::check_resolve()const
{
   clear_mrk( _root );
   struct check_resolve chk;
   clause_preorder( chk , _root) ;
}
void QProof::check_inorder()const
{
   clear_mrk( _root );
   clause_preorder( ::check_inorder(_lvl) , _root );
}
void QProof::check_connect()const
{
   clear_mrk( _root );
   clause_preorder( ::check_connect() , _root );

   clear_mrk( _root );

   vector<Clause * > cls;
   clause_preorder( get_cls( cls ) , _root );

   for( unsigned i = 0 ; i < cls.size() ; ++ i )
      for( unsigned j = 0 ; j < cls[i]->out.size() ; ++ j ){
         assert( cls[i]->out[j]->mrk == 1 );
      }
   clear_mrk( _root );
}
void QProof::plot( const char * file )const
{
   clear_mrk( _root );

   std::ofstream out( file );
   out << "graph dot{" << endl;
   clause_preorder( ::plot( out ) , _root);
   out << "}";
}

//=============================================================================
//      QProof Operation 
//=============================================================================

void QProof::swap_cls(
      Clause * a_b  ,  Clause * a_nb , 
      Clause * na  ,   Clause * a   , Clause * z   ,
      plit_t la , plit_t lb 
      )
{
   int exist = check_exist( *na , var(lb) );
   Clause * nz;
   if( exist != -1 )
   {
      Clause * bx = (exist^sign(lb))?a_nb:a_b;
      if( check_exist( *bx , var(la) ) == -1 )
         nz = bx;
      else
      {
         nz = new Clause( bx , na , la , _lut );
         if( nz->inorder( _lvl ) == false ) _stand_area.push_back( nz );
      }
   }else
   {
      Clause * b , * nb ;
     
      if( check_exist( *a_b , var(la) ) != -1 )
      {
         b = new Clause( a_b , na , la , _lut );
         if( b->inorder( _lvl ) == false ) _stand_area.push_back( b );
      }
      else
         b = a_b; 
   
      if( check_exist( *a_nb , var(la) ) != -1  )
      {
         nb = new Clause( a_nb , na , la , _lut );
         if( nb->inorder( _lvl ) == false ) _stand_area.push_back( nb );
      }
      else 
         nb = a_nb ;
       
      nz = new Clause( b , nb , lb , _lut );
      if( nz->inorder( _lvl ) == false ) _stand_area.push_back( nz );
   }
   if( z == _root ) _root = nz ;
   z->replace( nz );
   shorten( nz );
}
void QProof::swap_cls( Clause * c )
{
   vector<Clause * > out = c->out;
   plit_t b = c->x;
   for( unsigned i = 0 ; i < out.size() ; ++i )
   {
      plit_t a = out[i]->x;
      Clause * nc ;
      if( out[i]->in[0] == c ) 
         nc = out[i]->in[1];
      else      
         nc = out[i]->in[0] , a = ~a;
      swap_cls( c->in[0] , c->in[1] , nc , c , out[i] , a , b );
   }
}
// return stable
void QProof::swap_cls_by_iterate() 
{
   unsigned cnt;
   do
   {
      cnt=0;

      clear_mrk( _root );
      vector<Clause *> c;
      clause_preorder( get_branch(c) , _root );
      //clause_postorder( get_branch(c) , _root );
      clear_mrk( _root );
   
      for( unsigned i = 0 ; i < c.size() ; ++ i )
      //for( int i = c.size()-1 ; i >=0  ; -- i )
         if( c[i]->del == 0 && (c[i]->inorder( _lvl ) == false ) )
         {
            cnt += 1;
            swap_cls( c[i] );
         }
   
      Clause::remove_remove();
   }while( cnt != 0 );
}
void QProof::swap_cls_by_propagate()
{
   clear_mrk( _root );
   vector<Clause * > & cls = _stand_area;
   clause_postorder( get_branch(cls) , _root  );
   clear_mrk( _root );
   unsigned j =0;
   for( unsigned i = 0 ; i < cls.size() ; ++ i )
      if( cls[i]->inorder( _lvl ) == false )
         cls[j++] = cls[i];
   cls.resize( j );

   while( _stand_area.size() )
   {
      Clause * c = _stand_area.back();
      _stand_area.pop_back();
      if( c->del ) continue;

      swap_cls( c );
   }
   Clause::remove_remove();
}
void QProof::shorten( Clause * x )
{
   if( _root == x ) 
   {
      return ;
   }
   for( unsigned i = 0 ; i < x->out.size() ; )
   {
      Clause * y = x->out[i];
      if( y->mrk == 1 ){ i+=1; continue;}

      if( check_exist( *x , var(y->x) ) != -1 )
      {
         if( y->slim( _lut ) ) 
            shorten( y );
         y->mrk = 1;
         i=0;
      }else
      {
         y->replace( x ); 
         i = 0;
      }
   }
   for( unsigned i = 0 ; i < x->out.size() ; ++ i )
   {
      assert( x->out[i]->mrk == 1 );
      x->out[i]->mrk = 0;
   }
   //assert( x->out.size() );
   if( x->out.size() == 0 )x->remove();
}
void QProof::interpolant( StrashAIG & ckt , int * base )
{
   clear_mrk( _root );
   clause_postorder( ::interpolant( ckt , base ) , _root );
   ckt._po.push( _root->itp );
}
